#include "cktinfo.h"
#include <cstring>

//____ Local function _________________________________________________________
//  
//  LvlMt , CapMt 
//
//=============================================================================

int CktInfo::LEVEL_CONSIDER = 2;
static const unsigned char sign_pos = 0x01;
static const unsigned char sign_neg = 0x02;
static const unsigned char sign_bi  = 0x03;
static const unsigned char sign_int = 0x04;

struct LvlMt
{
   level_t * lvl;
   unsigned * focnt;
   LvlMt( level_t * c , unsigned * f  ):lvl(c),focnt(f){}
   bool operator()(AigLit a,AigLit b)const
   {
      if( lvl[var(a)] > lvl[var(b)] ) return true;
      if( lvl[var(a)] < lvl[var(b)] ) return false;
      return focnt[ var(a) ] < focnt[ var(b) ] ;
   }
};
struct CapMt
{
   level_t * level;
   level_t * arrival;
   CapMt( level_t * l , level_t * a ) : level( l ) , arrival( a ) {}
   bool operator()( AigLit a , AigLit b )const
   {
      return level[var(a)]+arrival[var(b)] > level[var(b)] + arrival[var(a)];
   }
};
//____ Initialize functions ___________________________________________________
//
//  creat fanout count : traverse , build 
//  reset level        : 
//
//=============================================================================
void CktInfo::init()
{
   LitUnion::init();
   LitUnion::validation( sz );
   _mrk.growTo( sz , 0 );
   create_focnt();
   reset_level();
}
void CktInfo::create_focnt()
{
   assert( _focnt.size() == 0 && _mrk.size() != 0 );

   unsigned * order = new unsigned [sz];
   int k = 0; 

   _focnt.growTo( _andFlag , 1 );
   _focnt.growTo( sz , 0 );
   unsigned * focnt = _focnt.data;
   
   for( unsigned i = 0 ; i < _po.size() ; ++i )
   {
      unsigned next = eqIdx( var( _po[i] ) );
      focnt[next] +=1 ;
      if( _mrk[ next ] == 0 )
      {
         _mrk[ next ] = 1;
         order[k++] = next;
      }
   }

   int ptr = 0;
   while( k != ptr )
   {
      unsigned n = order[ ptr ++ ];
      if( n < _andFlag ) continue; 
      for( unsigned i = 0 ; i < 2 ; ++ i )
      {
         unsigned next = eqInIdx( n , i ) ;
         focnt[next] +=1 ;
         if( _mrk[ next ] == 0 )
         {
            _mrk[ next ] = 1 ; 
            order[ k ++ ] = next;
         }
      }
   }
   delete [] order;
   memset( _mrk.data , 0 , _mrk.sz * sizeof( mark_t ) );
}
void CktInfo::reset_level()
{
   assert( _level.size() == 0 && _rlevel.size() == 0 );

   _level.resize( _andFlag , 1 );
   _level.growTo( size() , 0 );

   _rlevel.resize( size(),0 );
   level_t * arrival = _rlevel.data;
   for( unsigned i = sz-1 ; i >= _andFlag ; -- i)
   {
      level_t carrival = arrival[i] + 1 ;
      for( int j = 0 ; j < 2 ; ++ j )
      {
         unsigned n = eqInIdx( i , j );
         if( arrival[n] < carrival ) arrival[n] = carrival;
      }
   }

   if( LEVEL_CONSIDER == 0 )
   {
      memcpy( _level.data , _rlevel.data , sizeof( level_t ) * _andFlag ); 
      _level[0]=1;
   }

   _max_level = 0;
   for( unsigned i = 1 ; i < _andFlag ; ++ i )
      if( _max_level < arrival[i] ) _max_level = arrival[i];
}
//____ factor a new circuit ___________________________________________________
//
//  topological traversal 
//  factor 
//
//=============================================================================
static int get_cyclic( unsigned * focnt , unsigned * level ,unsigned size , unsigned andFlag )
{
	int maxidx = 0 , lvl = -1 ;
	for( unsigned i = size-1 ; i >= andFlag ; -- i )
		if( focnt[i] != 0 && (((int)level[i]) > lvl ) )
			maxidx = i , lvl = level[i];
	return maxidx;
}
void replace_cycle(  unsigned a , unsigned b , CktInfo & info )
{
	unsigned focnt=0;
	std::swap( info._focnt[a] , focnt );
	info.replace( a , b , focnt );
	if( info._focnt[a] != 0 ) info._focnt[b]-=1,info._focnt[a]+=1;
}
unsigned CktInfo::remove_cyclic( unsigned target , unsigned idx )
{
	if( eqIdx( idx ) == target ) return idx;
	if( _focnt[target] == 0 || idx < _andFlag ) return 0;

	unsigned eqidx = eqIdx(idx);
	unsigned ret;

	for( int i = 0 ; i < 2 ; ++ i )
		if( ret=remove_cyclic( target ,  var(data[eqidx].fanin[i]) ) )
		{
			if( eqidx != idx ) replace_cycle( eqidx , idx , *this );
			else return ret;
		}

	return 0;
}
unsigned cyclvl( unsigned x , unsigned * cyc , CktInfo & info )
{
	if( cyc[x] == 0x80000000 ) 
	{
		cyc[x] +=1;
		cyc[x] = std::max( cyclvl( info.eqInIdx(x,0) , cyc , info ) , cyclvl( info.eqInIdx(x,1),cyc,info) )+1;
	}
	return cyc[x];
}

int get_idx( vec<unsigned> & v , unsigned idx )
{
	for( unsigned i =0;i<v.size();++i)if(v[i]==idx)return i;return-1;
}
unsigned get_min( vec<unsigned> & v , unsigned * cyc )
{
	unsigned idx = v[0] , min = cyc[ idx ];
	for( unsigned i = 1 ; i < v.size() ; ++ i )
		if( cyc[ v[i] ] < min )
			idx=v[i],min=cyc[idx];
	return idx;
}
void CktInfo::factor( StrashAIG & ckt )
{
	vec<unsigned> ord(sz);ord.clear();
	unsigned idx;

	{
		unsigned * cyc = new unsigned[sz];
		for( unsigned i = 0 ; i < _andFlag ; ++ i ) cyc[i] = 1;
		for( unsigned i = _andFlag ; i < sz ; ++ i) cyc[i] = 0x80000000;
		for( unsigned i = 0 ; i < _po.size() ; ++ i ) 
			cyclvl( eqIdx(var(_po[i])) , cyc , *this );

		vec<unsigned> v;
		for( unsigned i = _andFlag ; i < sz ; ++ i ) if( _focnt[i] && cyc[i] >= 0x80000000 ) v.push( i );
		
		while( v.size() )
		{
			idx = get_min( v , cyc );
			for( int i = 0 ; i < 2 ; ++ i )
			{
				unsigned ret = remove_cyclic( idx , var(data[idx].fanin[i]) );
				if( ret )
				{
					assert( eqIdx(ret)==idx );
					replace_cycle( idx , ret , *this ); idx=ret;
					break;
				}
			}
			for(unsigned i=0;i<v.size();++i)cyc[v[i]]=0x80000000;
			for(unsigned i=0;i<v.size();++i)cyclvl(v[i],cyc,*this);
			v.sz=0;
			for( unsigned i = _andFlag ; i < sz ; ++ i ) if( _focnt[i] && cyc[i] >= 0x80000000 ) v.push( i );
		};
	}
	{
		unsigned ptr=0;
		for( unsigned i = 0 ; i < _po.size() ; ++ i )
		{
			idx = eqIdx(var(_po[i]));
			if( idx >= _andFlag && ( (_focnt[idx]-=1)==0 ) )
				ord.push(idx);
		}
		while( ptr != ord.size() )
		{
			unsigned n = ord[ptr++];
			for( unsigned i = 0 ; i < 2 ;++i)
			{
				idx = eqInIdx(n,i);
				if( idx >= _andFlag && ( (_focnt[idx]-=1)==0 ) )
					ord.push(idx);
			}
		}
	}
	{
		AigLit * lut = new AigLit[sz];
#ifndef NDEBUG
		memset( lut , -1 , sizeof(AigLit)*sz);
#endif
		lut[0] = 0; 
		for( unsigned i = 1 ; i < _andFlag;++i)
			ckt.createBase() , lut[i] = toAigLit(i,0);
		ckt._andFlag = _andFlag , ckt._ppiFlag = _ppiFlag;
	
		for( int i = ord.size()-1; i>=0 ;--i)
		{
			idx = ord[i];
			AigLit in[2] = { eqIn( idx , 0 ) , eqIn(idx,1) };
			assert( var(lut[var(in[0])]) < 0x10000000 && var(lut[var(in[1])]) < 0x10000000 );
			lut[ idx ] = ckt.createAND( lut[ var(in[0]) ] ^ sign(in[0]) , lut[ var(in[1]) ]^ sign(in[1] ));
		}
		for( unsigned i = 0 ; i < _po.size(); ++i)
		{
			AigLit eqo = eq(_po[i]);
			ckt._po.push( lut[var(eqo)]^sign(eqo) );
		}
	   delete [] lut;
	}

}
//____ simple update functions ________________________________________________
//
//  capacity update 
//  rlevel recover 
//  level queraing 
//
//=============================================================================
void CktInfo::validation()
{
   LitUnion::validation( sz );
   _mrk.resize( sz , 0 );
   _focnt.resize( sz, 0 );
   _level.resize( sz , 0 );
   _rlevel.resize( sz , 0 );
}
//--- event propagate
// the _mrk here is to avoid the cyclic situation 
void CktInfo::rlevel_recover( unsigned n )
{
	if( _mrk[n] ){ assert( _mrk[n] == 32 ); return ;} // avoid cyclic recover 
	_mrk[n] = 32 ;
   for( int i = 0 ; i < 2 ; ++ i )
   {
      unsigned m = eqInIdx(n,i);
      if( _rlevel[m] <= _rlevel[n] )
      { 
         _rlevel[m] = _rlevel[n]+1;
         if( m >= _andFlag)rlevel_recover(m);
      }
   }
	_mrk[n] = 0; 
}
//--- recursive construction
unsigned CktInfo::lvl( unsigned n )
{
   if( _level[n] == 0 )
      _level[n] = std::max( lvl( eqInIdx(n,0) ) , lvl( eqInIdx(n,1) ) ) + 1;
   return _level[n];
}
void CktInfo::update_level( unsigned n )
{
   _level[n] = std::max( _level[ var( data[n].fanin[0])]  , _level[ var( data[n].fanin[1]) ] ) + 1;
}
//____ Traversing Functions ___________________________________________________
//
//
//=============================================================================
void CktInfo::resume( unsigned * cone , unsigned s )
{
   for( unsigned i = 0 ; i < s ;++i)
   {
      unsigned n = cone[i];
      _focnt[ eqInIdx(n,0) ] += 1;
      _focnt[ eqInIdx(n,1) ] += 1;
   }
}
void CktInfo::rm_cone( unsigned n )
{ 
   if( (-- _focnt[eqInIdx(n,0)]) == 0 )rm_cone( eqInIdx(n,0) );
   n=eqInIdx(n,1);
   if( (-- _focnt[n]) == 0 )rm_cone(n);
}
unsigned CktInfo::get_cone( unsigned next , vec<unsigned> & cone)
{ 
   assert( _focnt[next] == 0 && _mrk.size() && _focnt.size() );
   cone.clear();

   if( ! _mrk[next] )
   {
      cone.push( next );

      unsigned ptr = 0 ;
      while( cone.size() != ptr )
      {
         unsigned node = cone[ptr++];
         for( unsigned j = 0 ; j < 2 ; ++ j)
         {
            next = eqInIdx( node , j );
            assert( _focnt[next] != 0 );
            _focnt[ next ] -=1 ;
            if( _focnt[ next ] == 0 && ! _mrk[ next ] )
               cone.push( next );
         }
      }
   }
   
   return cone.size();
}
unsigned CktInfo::get_freeCone( unsigned next , vec<unsigned> & cone)
{
   assert( _mrk.size() && _focnt.size() );
   cone.clear();

   if( _focnt[next] == 0 && ! _mrk[next] )
   {
      cone.push( next );
      _mrk[ next ] = 1; 

      unsigned ptr = 0 ;
      while( cone.size() != ptr )
      {
         unsigned node = cone[ptr++];
         for( unsigned j = 0 ; j < 2 ; ++ j)
         {
            next = eqInIdx( node , j );
            if( _focnt[ next ] == 0 && ! _mrk[ next ] )
            {
               cone.push( next );
               _mrk[next] = 1; 
            }
         }
      }
      for( unsigned i = 0 ; i < cone.size() ; ++i )
         _mrk[ cone[i] ] = 0; 
   }
   
   return cone.size();
}
void CktInfo::replace( unsigned n , unsigned p , unsigned focnt )
{
   assert( n == eqIdx(n) && _mrk.size() != 0 && _focnt[n] == 0 && p != n );
   unsigned eqp = eqIdx( p );
   if( eqp!=n) p = eqp;

   if( LEVEL_CONSIDER == 2 && _rlevel[p] < _rlevel[n] )
   {
      _rlevel[p] = _rlevel[n];
      if( p >= _andFlag )rlevel_recover( p );
   }

   get_freeCone( p , _tmp_cone);
   resume( _tmp_cone.data , _tmp_cone.sz );
   _focnt[p] += focnt;
   rm_cone( n );

   conjunct( n , p );
}
//____ Balance Construction  __________________________________________________
//
//
//=============================================================================
bool CktInfo::todo( unsigned idx )
{
   AigLit node[2] = { eqIn( idx , 0 ) , eqIn( idx ,1 ) };
   unsigned c = node[0] ^ node[1];
   
   if( (c & (~1)) == 0  )
   {
      c = c?0:var(node[0]);
      conjunct( idx , c );
      _focnt[ c ] += _focnt[ idx ]-2;
      _focnt[ idx ]=0;
      if( c == 0 ){ _focnt[0]+=2 ; rm_cone( idx );}
      return 0;
   }
   return _focnt[ var(node[0]) ] == 1 || _focnt[ var(node[1]) ] == 1 ;
}
AigLit CktInfo::build_blAND( AigLit * q , unsigned k )
{
   if( k < 3 )
   {
      if( k == 1 ) return q[0];
      if( k == 2 ){ AigLit p = createAND( q[0] , q[1] ); validation(); return p;}
   }

   for( unsigned i = 0 ; i < k ; ++ i )
      if( _level[ var(q[i]) ] == 0 ) lvl( var(q[i]) );
   std::sort( q , q+k , LvlMt( _level.data , _focnt.data ) );
   //std::sort( q , q+k , CapMt( _level.data , _rlevel.data ) );

   k-=1;
   while(k)
   {
      int i , t = std::max( (int)k-64 , 0 );
      for(i=k-2;i>=t;--i)
      {
         unsigned v = var( test_createAND(q[k],q[i]));
         if( v < _focnt.sz && _focnt[v] != 0 )
         {
            std::swap( q[i] , q[k-1] );
            break;
         }
      }
      k-=1;

      q[k] = createAND( q[k],q[k+1]);
      validation(); // lvl must increase 
      lvl( var(q[k]) );//update level
      for(i = k ; i > 0 ; -- i )
         if( _level[var(q[i])] > _level[var(q[i-1])] )
            std::swap( q[i],q[i-1]);
         else break;
   }
   return q[0];
}
